(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 4))
(declare-fun v3 () (_ BitVec 6))
(declare-fun a4 () (Array  (_ BitVec 2)  (_ BitVec 11)))
(assert (let ((e5(_ bv11161 14)))
(let ((e6(_ bv89 7)))
(let ((e7 (bvadd e6 ((_ zero_extend 3) v0))))
(let ((e8 (bvmul e7 e6)))
(let ((e9 (ite (distinct v0 v0) (_ bv1 1) (_ bv0 1))))
(let ((e10 ((_ rotate_right 3) v3)))
(let ((e11 ((_ sign_extend 6) v1)))
(let ((e12 (bvashr ((_ sign_extend 2) v2) e10)))
(let ((e13 (bvsrem e7 e7)))
(let ((e14 (bvxor e8 e6)))
(let ((e15 (bvnand ((_ zero_extend 10) v0) e5)))
(let ((e16 (store a4 ((_ extract 3 2) v2) ((_ sign_extend 10) e9))))
(let ((e17 (select a4 ((_ extract 4 3) v1))))
(let ((e18 (select a4 ((_ extract 1 0) v2))))
(let ((e19 (select e16 ((_ extract 5 4) e17))))
(let ((e20 (store a4 ((_ extract 12 11) e11) ((_ zero_extend 5) e10))))
(let ((e21 (select a4 ((_ sign_extend 1) e9))))
(let ((e22 (select a4 ((_ extract 3 2) e14))))
(let ((e23 (bvshl ((_ sign_extend 7) v0) e17)))
(let ((e24 (bvshl ((_ zero_extend 5) e10) e23)))
(let ((e25 (ite (bvule e8 e6) (_ bv1 1) (_ bv0 1))))
(let ((e26 (bvxnor ((_ sign_extend 4) e14) e18)))
(let ((e27 ((_ rotate_left 2) e7)))
(let ((e28 (bvcomp e11 ((_ sign_extend 5) e21))))
(let ((e29 (ite (= ((_ sign_extend 7) e13) e5) (_ bv1 1) (_ bv0 1))))
(let ((e30 (bvlshr ((_ sign_extend 15) e9) e11)))
(let ((e31 (ite (bvsge v3 ((_ zero_extend 5) e28)) (_ bv1 1) (_ bv0 1))))
(let ((e32 ((_ zero_extend 2) e19)))
(let ((e33 (bvsrem ((_ zero_extend 2) e22) e32)))
(let ((e34 ((_ extract 0 0) e12)))
(let ((e35 (ite (bvsle ((_ zero_extend 5) e24) e30) (_ bv1 1) (_ bv0 1))))
(let ((e36 ((_ zero_extend 0) e5)))
(let ((e37 (ite (bvsle ((_ zero_extend 5) e17) e30) (_ bv1 1) (_ bv0 1))))
(let ((e38 (ite (bvsle ((_ zero_extend 12) e28) e33) (_ bv1 1) (_ bv0 1))))
(let ((e39 ((_ zero_extend 1) v1)))
(let ((e40 (bvashr e15 ((_ zero_extend 13) e31))))
(let ((e41 (ite (bvugt ((_ sign_extend 10) e9) e17) (_ bv1 1) (_ bv0 1))))
(let ((e42 ((_ sign_extend 4) e6)))
(let ((e43 (ite (bvsle e23 ((_ sign_extend 10) e41)) (_ bv1 1) (_ bv0 1))))
(let ((e44 (bvashr ((_ sign_extend 10) v2) e36)))
(let ((e45 (bvult v1 ((_ sign_extend 3) e13))))
(let ((e46 (bvsge e5 ((_ zero_extend 10) v0))))
(let ((e47 (bvslt e38 e38)))
(let ((e48 (bvsle e11 ((_ zero_extend 3) e32))))
(let ((e49 (bvuge ((_ zero_extend 6) e29) e7)))
(let ((e50 (bvugt e18 ((_ zero_extend 1) v1))))
(let ((e51 (bvsle ((_ zero_extend 4) e7) e21)))
(let ((e52 (bvsgt e36 ((_ sign_extend 7) e6))))
(let ((e53 (distinct v2 ((_ zero_extend 3) e35))))
(let ((e54 (bvugt ((_ zero_extend 5) e23) e11)))
(let ((e55 (bvult ((_ sign_extend 7) e6) e5)))
(let ((e56 (= e13 e14)))
(let ((e57 (bvsle ((_ sign_extend 5) e12) e19)))
(let ((e58 (bvuge e32 e32)))
(let ((e59 (= ((_ sign_extend 12) e43) e32)))
(let ((e60 (bvsle e30 ((_ sign_extend 9) e8))))
(let ((e61 (bvsge e15 ((_ sign_extend 13) e31))))
(let ((e62 (bvsge e26 e21)))
(let ((e63 (bvule e33 ((_ zero_extend 2) e39))))
(let ((e64 (bvuge ((_ sign_extend 10) e10) e11)))
(let ((e65 (bvsge e30 ((_ zero_extend 15) e41))))
(let ((e66 (bvuge e32 ((_ zero_extend 12) e28))))
(let ((e67 (bvslt e5 ((_ sign_extend 3) e17))))
(let ((e68 (bvslt e5 ((_ sign_extend 10) v0))))
(let ((e69 (bvugt e27 e8)))
(let ((e70 (bvsgt ((_ sign_extend 8) e10) e5)))
(let ((e71 (bvsgt e6 ((_ zero_extend 6) e25))))
(let ((e72 (bvsge ((_ sign_extend 13) e9) e5)))
(let ((e73 (= e39 ((_ zero_extend 1) v1))))
(let ((e74 (bvslt e39 ((_ zero_extend 10) e31))))
(let ((e75 (distinct e31 e31)))
(let ((e76 (bvsgt ((_ zero_extend 13) e41) e5)))
(let ((e77 (distinct e24 ((_ zero_extend 10) e28))))
(let ((e78 (bvule e23 e39)))
(let ((e79 (bvsge ((_ sign_extend 8) v3) e5)))
(let ((e80 (bvuge ((_ zero_extend 3) e22) e15)))
(let ((e81 (bvsle ((_ zero_extend 6) e29) e27)))
(let ((e82 (bvsle e26 e18)))
(let ((e83 (bvsge e14 ((_ zero_extend 6) e43))))
(let ((e84 (distinct ((_ sign_extend 6) e34) e6)))
(let ((e85 (bvsgt ((_ sign_extend 3) e18) e15)))
(let ((e86 (= e33 ((_ sign_extend 6) e7))))
(let ((e87 (bvugt ((_ sign_extend 10) e37) e24)))
(let ((e88 (bvsgt ((_ sign_extend 4) e13) e24)))
(let ((e89 (bvsgt ((_ sign_extend 10) e31) e19)))
(let ((e90 (bvsle ((_ zero_extend 1) v3) e13)))
(let ((e91 (bvugt ((_ sign_extend 4) e13) e22)))
(let ((e92 (bvsle e15 ((_ zero_extend 8) e12))))
(let ((e93 (bvult ((_ sign_extend 5) e37) e10)))
(let ((e94 (bvule e36 e44)))
(let ((e95 (distinct e37 e43)))
(let ((e96 (bvsle ((_ sign_extend 7) v3) e32)))
(let ((e97 (bvsgt e12 ((_ sign_extend 5) e43))))
(let ((e98 (bvuge ((_ zero_extend 3) e31) v0)))
(let ((e99 (bvsgt e25 e28)))
(let ((e100 (bvule e15 ((_ sign_extend 1) e32))))
(let ((e101 (bvsle e36 e36)))
(let ((e102 (bvule e40 ((_ zero_extend 13) e34))))
(let ((e103 (distinct e18 ((_ sign_extend 4) e14))))
(let ((e104 (bvsge ((_ sign_extend 5) e21) e11)))
(let ((e105 (bvuge e11 ((_ zero_extend 9) e27))))
(let ((e106 (bvule ((_ sign_extend 5) v3) e18)))
(let ((e107 (bvuge e21 e22)))
(let ((e108 (distinct e14 e13)))
(let ((e109 (bvult e26 ((_ zero_extend 10) e9))))
(let ((e110 (distinct v1 ((_ zero_extend 3) e8))))
(let ((e111 (bvslt ((_ zero_extend 5) e23) e11)))
(let ((e112 (bvuge e29 e35)))
(let ((e113 (bvsle e34 e34)))
(let ((e114 (bvult ((_ sign_extend 7) v0) e22)))
(let ((e115 (distinct ((_ zero_extend 2) e36) e11)))
(let ((e116 (bvult ((_ sign_extend 12) e25) e33)))
(let ((e117 (bvslt ((_ zero_extend 7) e14) e40)))
(let ((e118 (bvuge e26 ((_ sign_extend 4) e14))))
(let ((e119 (= e39 ((_ sign_extend 1) v1))))
(let ((e120 (distinct e44 ((_ sign_extend 3) e22))))
(let ((e121 (bvugt e22 e39)))
(let ((e122 (bvugt e13 ((_ zero_extend 6) e34))))
(let ((e123 (distinct e24 ((_ sign_extend 7) v0))))
(let ((e124 (bvult e22 ((_ sign_extend 10) e28))))
(let ((e125 (bvuge e5 ((_ zero_extend 1) e33))))
(let ((e126 (bvslt ((_ sign_extend 4) e6) e21)))
(let ((e127 (bvuge e22 ((_ sign_extend 7) v2))))
(let ((e128 (bvslt e8 ((_ sign_extend 6) e31))))
(let ((e129 (distinct ((_ zero_extend 2) e19) e32)))
(let ((e130 (distinct ((_ sign_extend 5) v3) e17)))
(let ((e131 (bvsge e40 ((_ zero_extend 10) v0))))
(let ((e132 (bvuge ((_ zero_extend 6) e37) e8)))
(let ((e133 (distinct e33 ((_ sign_extend 2) e23))))
(let ((e134 (bvule e11 ((_ zero_extend 2) e44))))
(let ((e135 (bvsgt ((_ zero_extend 5) v3) e18)))
(let ((e136 (bvsge ((_ sign_extend 5) e35) e12)))
(let ((e137 (bvslt ((_ sign_extend 4) e6) e22)))
(let ((e138 (bvule e36 e15)))
(let ((e139 (bvule ((_ sign_extend 15) e34) e30)))
(let ((e140 (bvuge ((_ zero_extend 7) v2) e42)))
(let ((e141 (xor e114 e128)))
(let ((e142 (ite e80 e135 e49)))
(let ((e143 (or e115 e50)))
(let ((e144 (=> e139 e124)))
(let ((e145 (or e105 e132)))
(let ((e146 (or e93 e103)))
(let ((e147 (not e78)))
(let ((e148 (xor e88 e137)))
(let ((e149 (ite e142 e59 e61)))
(let ((e150 (or e87 e63)))
(let ((e151 (xor e52 e85)))
(let ((e152 (xor e56 e144)))
(let ((e153 (xor e127 e72)))
(let ((e154 (= e126 e67)))
(let ((e155 (not e77)))
(let ((e156 (or e71 e134)))
(let ((e157 (= e109 e81)))
(let ((e158 (and e65 e68)))
(let ((e159 (not e75)))
(let ((e160 (ite e66 e58 e47)))
(let ((e161 (or e120 e94)))
(let ((e162 (ite e90 e104 e101)))
(let ((e163 (xor e117 e92)))
(let ((e164 (= e73 e152)))
(let ((e165 (ite e138 e150 e97)))
(let ((e166 (and e48 e129)))
(let ((e167 (= e91 e163)))
(let ((e168 (not e130)))
(let ((e169 (=> e145 e156)))
(let ((e170 (= e159 e123)))
(let ((e171 (and e84 e133)))
(let ((e172 (xor e164 e86)))
(let ((e173 (or e53 e166)))
(let ((e174 (and e69 e110)))
(let ((e175 (ite e116 e140 e161)))
(let ((e176 (and e55 e143)))
(let ((e177 (ite e99 e162 e98)))
(let ((e178 (ite e125 e165 e57)))
(let ((e179 (ite e70 e173 e177)))
(let ((e180 (not e54)))
(let ((e181 (ite e111 e113 e89)))
(let ((e182 (=> e176 e169)))
(let ((e183 (or e153 e79)))
(let ((e184 (ite e179 e118 e46)))
(let ((e185 (xor e184 e160)))
(let ((e186 (not e154)))
(let ((e187 (=> e174 e121)))
(let ((e188 (xor e151 e96)))
(let ((e189 (not e170)))
(let ((e190 (or e106 e131)))
(let ((e191 (ite e186 e51 e189)))
(let ((e192 (not e190)))
(let ((e193 (= e158 e185)))
(let ((e194 (not e83)))
(let ((e195 (= e122 e180)))
(let ((e196 (xor e102 e82)))
(let ((e197 (ite e194 e108 e136)))
(let ((e198 (not e196)))
(let ((e199 (not e181)))
(let ((e200 (=> e198 e45)))
(let ((e201 (or e191 e191)))
(let ((e202 (ite e62 e195 e146)))
(let ((e203 (ite e168 e60 e95)))
(let ((e204 (= e199 e64)))
(let ((e205 (xor e175 e197)))
(let ((e206 (xor e157 e187)))
(let ((e207 (= e107 e205)))
(let ((e208 (and e172 e204)))
(let ((e209 (xor e100 e171)))
(let ((e210 (ite e119 e203 e202)))
(let ((e211 (xor e147 e149)))
(let ((e212 (= e206 e155)))
(let ((e213 (and e178 e211)))
(let ((e214 (= e200 e148)))
(let ((e215 (not e112)))
(let ((e216 (and e213 e76)))
(let ((e217 (and e209 e212)))
(let ((e218 (ite e216 e208 e188)))
(let ((e219 (and e201 e167)))
(let ((e220 (and e182 e214)))
(let ((e221 (and e219 e141)))
(let ((e222 (not e217)))
(let ((e223 (and e222 e218)))
(let ((e224 (= e74 e210)))
(let ((e225 (not e183)))
(let ((e226 (and e221 e220)))
(let ((e227 (and e224 e226)))
(let ((e228 (not e215)))
(let ((e229 (xor e223 e228)))
(let ((e230 (and e225 e193)))
(let ((e231 (or e230 e229)))
(let ((e232 (xor e231 e231)))
(let ((e233 (ite e192 e227 e232)))
(let ((e234 (and e207 e207)))
(let ((e235 (and e234 e233)))
(let ((e236 (and e235 (not (= e7 (_ bv0 7))))))
(let ((e237 (and e236 (not (= e7 (bvnot (_ bv0 7)))))))
(let ((e238 (and e237 (not (= e32 (_ bv0 13))))))
(let ((e239 (and e238 (not (= e32 (bvnot (_ bv0 13)))))))
e239
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
